(*
** Implementacion de Mini-AES en el lenguaje definido en Lang.v.
*)

Require Import TypesImpl.
Open Scope Z_scope.
Open Scope lang_scope.


Module MiniAes.

Definition a0 := id 1.
Definition b0 := id 2.
Definition sbox := id 3.
Definition aux := id 4.
Definition a00 := id 5.
Definition b00 := id 6.
Definition a01 := id 7.
Definition b01 := id 8.
Definition a10 := id 9.
Definition b10 := id 10.
Definition a11 := id 11.
Definition b11 := id 12.

Definition key_addition(text key: Id) :=
  text[0][0] ::= text[0][0] xor key[0][0];
  text[0][1] ::= text[0][1] xor key[0][1];
  text[1][0] ::= text[1][0] xor key[1][0];
  text[1][1] ::= text[1][1] xor key[1][1];
.

Definition nibble_sub (text sbox: Id) :=
  byte a00   ::= text[0][0];
  byte b00   ::= sbox[0][a00];
  text[0][0] ::= b00;

  byte a01   ::= text[0][1];
  byte b01   ::= sbox[0][a01];
  text[0][1] ::= b01;

  byte a10   ::= text[1][0];
  byte b10   ::= sbox[0][a10];
  text[1][0] ::= b10;

  byte a11   ::= text[1][1];
  byte b11   ::= sbox[0][a11];
  text[1][1] ::= b11;
.

Definition shift_row (text: Id) :=
  byte aux   ::= text[1][0];
  text[1][0] ::= (text[1][1]);
  text[1][1] ::= aux;
. 

Definition mix_columns (text mult_table: Id) :=
  byte a00   ::= text[0][0];
  byte a10   ::= text[1][0];
  text[0][0] ::= mult_table[a00][a10];
  text[1][0] ::= mult_table[a10][a00];

  byte a01   ::= text[0][1];
  byte a11   ::= text[1][1];
  text[0][1] ::= mult_table[a01][a11];
  text[1][1] ::= mult_table[a11][a01];
.

Definition encrypt (text sbox mult_table key_0 key_1 key_2: Id) :=
  key_addition text key_2;
  nibble_sub   text sbox;
  shift_row    text;
  mix_columns  text mult_table;
  key_addition text key_1;
  nibble_sub   text sbox;
  shift_row    text;
  key_addition text key_0;
.

Definition decrypt (cipher_text sbox_inv mult_table key_0 key_1 key_2: Id) :=
  key_addition cipher_text key_0;
  shift_row    cipher_text;
  nibble_sub   cipher_text sbox_inv;
  key_addition cipher_text key_1;
  mix_columns  cipher_text mult_table;
  shift_row    cipher_text;
  nibble_sub   cipher_text sbox_inv;
  key_addition cipher_text key_2;
.

End MiniAes.
